Nuprl Lemma : rps_wf
11,40
postcript
pdf
x
,
y
:int_seg(0; 3). rps(
x
;
y
)
latex
Definitions
rps(
x
;
y
)
,
bor(
p
;
q
)
,
band(
p
;
q
)
,
(
i
=
j
)
,
x
:
A
B
(
x
)
,
{
x
:
A
|
B
(
x
)}
,
int_seg(
i
;
j
)
,
x
:
A
.
B
(
x
)
,
t
T
,
#$n
Lemmas
int
seg
wf
,
eq
int
wf
,
band
wf
,
bor
wf
origin
x,y:int_seg(0; 3). rps(x; y) 
x,y:int_seg(0; 3). rps(x; y) 
j)
B(x)x:A. B(x) T